x:(), r:, k:, y:( List).
(k  ||y||)
 (x(k) = 0  )
 (q-rel(r;q-linear(k;j.x(j);y))  q-rel(r;q-linear(k - 1;j.x(j);y))) 

latex

Definitions	T, P  Q, P & Q, x. t(x), False, A, True, , t  T, P  Q, A  B, P  Q, , x:A. B(x), x(s), , S  T
Lemmas	mon ident q, qadd comm q, qmul zero qrng, q-linear-unroll, true wf, squash wf, select wf, qmul wf, qadd wf, iff wf, q-linear wf, q-rel wf, nat wf, nat plus wf, length wf1, le wf, int inc rationals, nat plus inc, rationals wf